l:IdLnk, k:Knd, tg:Id, v:Top. k  dom(lnk-decl(l;tg : v)) ~ rcv(l,tg) = k 

latex

Definitions	x:AB(x), P  Q, x:A. B(x), , s = t, b, A, x:A  B(x), P & Q, P  Q, t  T, Unit, left + right, x  dom(f), lnk-decl(l;dt), x : v, Top, Id, Knd, IdLnk, rcv(l,tg), a = b
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot